COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 match.lsp[w82,jmc]	ekl axioms and proof about match and sublisq
C00010 ENDMK
C⊗;
;;; match.lsp[w82,jmc]	ekl axioms and proof about match and sublisq

(wipe-out)
(get-proofs lispax)
(proof match)
(context lispax#1:*)

(decl (pat exp) ground)
(decl (NO QUOTE LOSE) ground constant sexp)

(decl (match) |ground⊗ground⊗ground → ground| constant)

(axiom |∀pat exp. match(pat, exp, NO) = NO|)
(lname definfo)

(axiom |∀ pat exp alist. match(pat,exp,alist) =
      if atom pat then
         (λa1.if null a1 then (pat~exp)~alist
              else if cdr car a1 = exp then alist
              else NO)
         (assoc(pat,alist))
      else if car pat = QUOTE then (if car cdr pat = exp then alist else NO)
      else if atom exp then NO
      else match(car pat, car exp, match(cdr pat, cdr exp, alist))|)
(lname definfo)

(decl sublisq |ground⊗ground → ground| constant)

(axiom |∀ pat alist. sublisq(pat, alist) =
      if atom pat then (λu.if null u then LOSE else cdr u)(assoc(pat,alist))
      else if car pat = QUOTE then car cdr pat
      else sublisq(car pat, alist) ~ sublisq(cdr pat, alist)|)
(lname definfo)

(decl matchp |ground⊗ground⊗ground → truthval|)
(axiom |∀pat exp alist.matchp(pat,exp,alist) ≡
       if atom pat then
         (λa1. null a1 ∨ cdr cdr a1 = exp)(assoc(pat,alist))
       else if car pat = QUOTE then (car cdr pat = exp)
       else ¬atom exp ∧ matchp(cdr pat, cdr exp, alist)
            ∧ matchp(car pat, car exp, match(cdr pat, cdr exp, alist))|)
(lname definfo)

(∀e phi |λpat.∀exp alist.match(pat, exp, alist) ≠ NO
       ⊃ sublisq(pat, match(pat, exp, alist)) = exp| lispax#sexpinduction nil)

(assume |match(pat, exp, alist) ≠ NO|)

(rw 12 |nil*$definfo*nil**simpinfo**sortinfo*nil| sortinfo)